(*  Title:     State.thy
    Author:    David Sanán, Trinity College Dublin, 2012
*)

section "Word Declarations"

theory WordDecl
imports Main "HOL-Library.Word"
begin

text ‹
This theory provides ‹len0› and ‹len› instantiations 
for the most common used word sizes in the model (1,2,4,5,6,8,12,16,18,20,24,32,36).
The ‹len0› class defines lengths that range from 0 upwards,
whilst the ‹len› class caters for non-zero lengths.
Bit-operators like ‹<<›, ‹>>›, ‹and›, or ‹or› 
require ‹a'::len› word instances,
while other word operations such @{term "ucast"} 
(gets an integer from a word) 
can be defined for ‹len0› words. 

For each length ‹N›, we:
  ▸ declare a type ‹word_lengthN›;
  ▸ make it an instance of both length classes;
  ▸ and introduce a short type synonym ‹wordN›, and a suitable translation.

In essence, this theory is just a lot of boilerplate.
\newpage
›

section "Words of length 1"

typedecl word_length1
instantiation word_length1 :: len0
begin
definition
  len1 [simp]: "len_of (x::word_length1 itself) ≡ 1"
instance .. 
end
instantiation word_length1 :: len
begin
instance by intro_classes simp
end
type_synonym word1 = "word_length1 word"
translations (type) "word1" <= (type) "word_length1 word"

subsection "Words of length 1's constants"

definition ONE::"word1"
where
"ONE ≡ 1"

definition ZERO::"word1"
where
"ZERO ≡ 0"

section "Words of length 2"

typedecl word_length2
instantiation word_length2 :: len0
begin
definition
  len2 [simp]: "len_of (x::word_length2 itself) ≡ 2"
instance .. 
end
instantiation word_length2 :: len
begin
instance by intro_classes simp
end
type_synonym word2 = "word_length2 word"
translations (type) "word2" <= (type) "word_length2 word"

section "Words of length 3"

typedecl word_length3
instantiation word_length3 :: len0
begin
definition
  len3 [simp]: "len_of (x::word_length3 itself) ≡ 3"
instance .. 
end
instantiation word_length3 :: len
begin
instance by intro_classes simp
end
type_synonym word3 = "word_length3 word"
translations (type) "word3" <= (type) "word_length3 word"

section "Words of length 4"

typedecl word_length4
instantiation word_length4 :: len0
begin
definition
  len4 [simp]: "len_of (x::word_length4 itself) ≡ 4"
instance .. 
end
instantiation word_length4 :: len
begin
instance by intro_classes simp
end
type_synonym word4 = "word_length4 word"
translations (type) "word4" <= (type) "word_length4 word"

section "Words of length 5"

typedecl word_length5
instantiation word_length5 :: len0
begin
definition
  len5 [simp]: "len_of (x::word_length5 itself) ≡ 5"
instance .. 
end
instantiation word_length5 :: len
begin
instance by intro_classes simp
end
type_synonym word5 = "word_length5 word"
translations (type) "word5" <= (type) "word_length5 word"

section "Words of length 6"

typedecl word_length6
instantiation word_length6 :: len0
begin
definition
  len6 [simp]: "len_of (x::word_length6 itself) ≡ 6"
instance .. 
end
instantiation word_length6 :: len
begin
instance by intro_classes simp
end
type_synonym word6 = "word_length6 word"
translations (type) "word6" <= (type) "word_length6 word"

section "Words of length 6"

typedecl word_length7
instantiation word_length7 :: len0
begin
definition
  len7 [simp]: "len_of (x::word_length7 itself) ≡ 7"
instance .. 
end
instantiation word_length7 :: len
begin
instance by intro_classes simp
end
type_synonym word7 = "word_length7 word"
translations (type) "word7" <= (type) "word_length7 word"

section "Words of length 8"

typedecl word_length8
instantiation word_length8 :: len0
begin
definition
  len8 [simp]: "len_of (x::word_length8 itself) ≡ 8"
instance .. 
end
instantiation word_length8 :: len
begin
instance by intro_classes simp
end
type_synonym word8 = "word_length8 word"
translations (type) "word8" <= (type) "word_length8 word"

section "Words of length 9"

typedecl word_length9
instantiation word_length9 :: len0
begin
definition
  len9 [simp]: "len_of (x::word_length9 itself) ≡ 9"
instance .. 
end
instantiation word_length9 :: len
begin
instance by intro_classes simp
end
type_synonym word9 = "word_length9 word"
translations (type) "word9" <= (type) "word_length9 word"

section "Words of length 10"

typedecl word_length10
instantiation word_length10 :: len0
begin
definition
  len10 [simp]: "len_of (x::word_length10 itself) ≡ 10"
instance .. 
end
instantiation word_length10 :: len
begin
instance by intro_classes simp
end
type_synonym word10 = "word_length10 word"
translations (type) "word10" <= (type) "word_length10 word"

section "Words of length 12"

typedecl word_length12
instantiation word_length12 :: len0
begin
definition
  len12 [simp]: "len_of (x::word_length12 itself) ≡ 12"
instance .. 
end
instantiation word_length12 :: len
begin
instance by intro_classes simp
end
type_synonym word12 = "word_length12 word"
translations (type) "word12" <= (type) "word_length12 word"

section "Words of length 13"

typedecl word_length13
instantiation word_length13 :: len0
begin
definition
  len13 [simp]: "len_of (x::word_length13 itself) ≡ 13"
instance .. 
end
instantiation word_length13 :: len
begin
instance by intro_classes simp
end
type_synonym word13 = "word_length13 word"
translations (type) "word13" <= (type) "word_length13 word"

section "Words of length 16"

typedecl word_length16
instantiation word_length16 :: len0
begin
definition
  len16 [simp]: "len_of (x::word_length16 itself) ≡ 16"
instance .. 
end
instantiation word_length16 :: len
begin
instance by intro_classes simp
end
type_synonym word16 = "word_length16 word"
translations (type) "word16" <= (type) "word_length16 word"

section "Words of length 18"

typedecl word_length18
instantiation word_length18 :: len0
begin
definition
  len18 [simp]: "len_of (x::word_length18 itself) ≡ 18"
instance .. 
end
instantiation word_length18 :: len
begin
instance by intro_classes simp
end
type_synonym word18 = "word_length18 word"
translations (type) "word18" <= (type) "word_length18 word"

section "Words of length 20"

typedecl word_length20
instantiation word_length20 :: len0
begin
definition
  len20 [simp]: "len_of (x::word_length20 itself) ≡ 20"
instance .. 
end
instantiation word_length20 :: len
begin
instance by intro_classes simp
end
type_synonym word20 = "word_length20 word"
translations (type) "word20" <= (type) "word_length20 word"

section "Words of length 22"

typedecl word_length22
instantiation word_length22 :: len0
begin
definition
  len22 [simp]: "len_of (x::word_length22 itself) ≡ 22"
instance .. 
end
instantiation word_length22 :: len
begin
instance by intro_classes simp
end
type_synonym word22 = "word_length22 word"
translations (type) "word22" <= (type) "word_length22 word"

section "Words of length 24"

typedecl word_length24
instantiation word_length24 :: len0
begin
definition
  len24 [simp]: "len_of (x::word_length24 itself) ≡ 24"
instance .. 
end
instantiation word_length24 :: len
begin
instance by intro_classes simp
end
type_synonym word24 = "word_length24 word"
translations (type) "word24" <= (type) "word_length24 word"

section "Words of length 30"

typedecl word_length30
instantiation word_length30 :: len0
begin
definition
  len30 [simp]: "len_of (x::word_length30 itself) ≡ 30"
instance .. 
end
instantiation word_length30 :: len
begin
instance by intro_classes simp
end
type_synonym word30 = "word_length30 word"
translations (type) "word30" <= (type) "word_length30 word"

section "Words of length 30"

typedecl word_length31
instantiation word_length31 :: len0
begin
definition
  len31 [simp]: "len_of (x::word_length31 itself) ≡ 31"
instance .. 
end
instantiation word_length31 :: len
begin
instance by intro_classes simp
end
type_synonym word31 = "word_length31 word"
translations (type) "word31" <= (type) "word_length31 word"

section "Words of length 32"

typedecl word_length32
instantiation word_length32 :: len0
begin
definition
  len32 [simp]: "len_of (x::word_length32 itself) ≡ 32"
instance .. 
end
instantiation word_length32 :: len
begin                            
instance by intro_classes simp
end
type_synonym word32 = "word_length32 word"
translations (type) "word32" <= (type) "word_length32 word"

section "Words of length 33"

typedecl word_length33
instantiation word_length33 :: len0
begin
definition
  len33 [simp]: "len_of (x::word_length33 itself) ≡ 33"
instance .. 
end
instantiation word_length33 :: len
begin                            
instance by intro_classes simp
end
type_synonym word33 = "word_length33 word"
translations (type) "word33" <= (type) "word_length33 word"

section "Words of length 36"

typedecl word_length36
instantiation word_length36 :: len0
begin
definition
  len36 [simp]: "len_of (x::word_length36 itself) ≡ 36"
instance ..
end
instantiation word_length36 :: len
begin
  instance by intro_classes simp
end
type_synonym word36 = "word_length36 word"
translations (type) "word36" <= (type) "word_length36 word"

section "Words of length 64"

typedecl word_length64
instantiation word_length64 :: len0
begin
definition
  len64 [simp]: "len_of (x::word_length64 itself) ≡ 64"
instance ..
end
instantiation word_length64 :: len
begin
  instance by intro_classes simp
end
type_synonym word64 = "word_length64 word"
translations (type) "word64" <= (type) "word_length64 word"

end

(*
 * Copyright 2016, NTU
 *
 * This software may be distributed and modified according to the terms of
 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
 * See "LICENSE_BSD2.txt" for details.
 *
 * Author: Zhe Hou, David Sanan. 
 *)

section ‹SPARC V8 architecture CPU model›
theory Sparc_Types    
imports Main "../lib/WordDecl" "Word_Lib.Traditional_Infix_Syntax"
begin

text ‹The following type definitions are taken from David Sanan's 
definitions for SPARC machines.›

type_synonym machine_word = word32
type_synonym byte = word8
type_synonym phys_address = word36

type_synonym virtua_address = word32
type_synonym page_address = word24
type_synonym offset = word12

type_synonym table_entry = word8

definition page_size :: "word32" where "page_size ≡ 4096"

type_synonym virtua_page_address = word20
type_synonym context_type = word8

type_synonym word_length_t1 = word_length8
type_synonym word_length_t2 = word_length6
type_synonym word_length_t3 = word_length6
type_synonym word_length_offset = word_length12
type_synonym word_length_page = word_length24
type_synonym word_length_phys_address = word_length36
type_synonym word_length_virtua_address = word_length32
type_synonym word_length_entry_type = word_length2
type_synonym word_length_machine_word = word_length32

definition length_machine_word :: "nat" 
 where "length_machine_word ≡ LENGTH(word_length_machine_word)"

text_raw ‹\newpage›

section ‹CPU Register Definitions›

text‹
 The definitions below come from the SPARC Architecture Manual, Version 8.
 The LEON3 processor has been certified SPARC V8 conformant (2005).
›

definition leon3khz ::"word32"
where
"leon3khz ≡ 33000"

text ‹The following type definitions for MMU is taken from 
David Sanan's definitions for MMU.›

text‹
  The definitions below come from the UT699 LEON 3FT/SPARC V8 Microprocessor Functional Manual, 
   Aeroflex, June 20, 2012, p35.
›
datatype MMU_register
 = CR    ― ‹Control Register›
 | CTP   ― ‹ConText Pointer register›
 | CNR   ― ‹Context Register›
 | FTSR   ― ‹Fault Status Register›
 | FAR   ― ‹Fault Address Register›

lemma MMU_register_induct: 
  "P CR ⟹ P CTP ⟹ P CNR ⟹ P FTSR ⟹ P FAR 
   ⟹ P x"
  by (cases x) auto

lemma UNIV_MMU_register [no_atp]: "UNIV = {CR, CTP, CNR, FTSR, FAR}"
   apply (safe)
   apply (case_tac x)
   apply (auto intro:MMU_register_induct)
  done


instantiation MMU_register :: enum begin

definition "enum_MMU_register = [ CR, CTP, CNR, FTSR, FAR ]"

definition
  "enum_all_MMU_register P ⟷ P CR ∧ P CTP ∧ P CNR ∧ P FTSR ∧ P FAR "
definition
  "enum_ex_MMU_register P ⟷ P CR ∨ P CTP ∨ P CNR ∨ P FTSR ∨ P FAR"

 instance proof
  qed (simp_all only: enum_MMU_register_def enum_all_MMU_register_def 
                      enum_ex_MMU_register_def UNIV_MMU_register, simp_all)
end
type_synonym MMU_context = "MMU_register ⇒ machine_word"

text ‹‹PTE_flags› is the last 8 bits of a PTE. See page 242 of SPARCv8 manual.
▪ C - bit 7
▪ M - bit 6,
▪ R - bit 5
▪ ACC - bit 4~2
▪ ET - bit 1~0.›

type_synonym PTE_flags = word8

text ‹
  @{term CPU_register} datatype is an enumeration with the CPU registers defined in the SPARC V8 
  architecture.
›
datatype CPU_register = 
   PSR   ― ‹Processor State Register›
 | WIM   ― ‹Window Invalid Mask›
 | TBR   ― ‹Trap Base Register›
 | Y     ― ‹Multiply/Divide Register›
 | PC    ― ‹Program Counter›
 | nPC   ― ‹next Program Counter›
 | DTQ   ― ‹Deferred-Trap Queue›
 | FSR   ― ‹Floating-Point State Register›
 | FQ    ― ‹Floating-Point Deferred-Trap Queue›
 | CSR   ― ‹Coprocessor State Register›
 | CQ    ― ‹Coprocessor Deferred-Trap Queue›
 (*| CCR   --   "Cache Control Register"*)
 | ASR "word5"  ― ‹Ancillary State Register›

text ‹The following two functions are dummies since we will not use 
        ASRs. Future formalisation may add more details to this.›

definition privileged_ASR :: "word5 ⇒ bool"
where
"privileged_ASR r ≡ False
"

definition illegal_instruction_ASR :: "word5 ⇒ bool"
where
"illegal_instruction_ASR r ≡ False
"

definition get_tt :: "word32 ⇒ word8"
where
"get_tt tbr ≡
  ucast (((AND) tbr 0b00000000000000000000111111110000) >> 4)
"

text ‹Write the tt field of the TBR register. 
        Return the new value of TBR.›
definition write_tt :: "word8 ⇒ word32 ⇒ word32"
where
"write_tt new_tt_val tbr_val ≡
  let tmp = (AND) tbr_val 0b111111111111111111111000000001111 in
      (OR) tmp (((ucast new_tt_val)::word32) << 4)
"

text ‹Get the nth bit of WIM. This equals ((AND) WIM $2^n$). 
        N.B. the first bit of WIM is the 0th bit.›
definition get_WIM_bit :: "nat ⇒ word32 ⇒ word1"
where
"get_WIM_bit n wim ≡
  let mask = ((ucast (0b1::word1))::word32) << n in
  ucast (((AND) mask wim) >> n)
"

definition get_CWP :: "word32 ⇒ word5"
where
"get_CWP psr ≡ 
  ucast ((AND) psr 0b00000000000000000000000000011111) 
"

definition get_ET :: "word32 ⇒ word1"
where
"get_ET psr ≡ 
  ucast (((AND) psr 0b00000000000000000000000000100000) >> 5) 
"

definition get_PIL :: "word32 ⇒ word4"
where
"get_PIL psr ≡ 
  ucast (((AND) psr 0b00000000000000000000111100000000) >> 8) 
"

definition get_PS :: "word32 ⇒ word1"
where
"get_PS psr ≡ 
  ucast (((AND) psr 0b00000000000000000000000001000000) >> 6) 
"

definition get_S :: "word32 ⇒ word1"
where
"get_S psr ≡ 
  ⌦‹ucast (((AND) psr 0b00000000000000000000000010000000) >> 7)›
  if ((AND) psr (0b00000000000000000000000010000000::word32)) = 0 then 0
  else 1
"

definition get_icc_N :: "word32 ⇒ word1"
where
"get_icc_N psr ≡
  ucast (((AND) psr 0b00000000100000000000000000000000) >> 23)
"

definition get_icc_Z :: "word32 ⇒ word1"
where
"get_icc_Z psr ≡
  ucast (((AND) psr 0b00000000010000000000000000000000) >> 22)
"

definition get_icc_V :: "word32 ⇒ word1"
where
"get_icc_V psr ≡
  ucast (((AND) psr 0b00000000001000000000000000000000) >> 21)
"

definition get_icc_C :: "word32 ⇒ word1"
where
"get_icc_C psr ≡
  ucast (((AND) psr 0b00000000000100000000000000000000) >> 20)
"

definition update_S :: "word1 ⇒ word32 ⇒ word32"
where
"update_S s_val psr_val ≡
  let tmp0 = (AND) psr_val 0b11111111111111111111111101111111 in
  (OR) tmp0 (((ucast s_val)::word32) << 7)
"

text ‹Update the CWP field of PSR. 
        Return the new value of PSR.›
definition update_CWP :: "word5 ⇒ word32 ⇒ word32"
where
"update_CWP cwp_val psr_val ≡
  let tmp0 = (AND) psr_val (0b11111111111111111111111111100000::word32);
      s_val = ((ucast (get_S psr_val))::word1)
  in
  if s_val = 0 then  
    (AND) ((OR) tmp0 ((ucast cwp_val)::word32)) (0b11111111111111111111111101111111::word32)
  else
    (OR) ((OR) tmp0 ((ucast cwp_val)::word32)) (0b00000000000000000000000010000000::word32)
"

text ‹Update the the ET, CWP, and S fields of PSR. 
        Return the new value of PSR.›
definition update_PSR_rett :: "word5 ⇒ word1 ⇒ word1 ⇒ word32 ⇒ word32"
where
"update_PSR_rett cwp_val et_val s_val psr_val ≡
  let tmp0 = (AND) psr_val 0b11111111111111111111111101000000;
      tmp1 = (OR) tmp0 ((ucast cwp_val)::word32);
      tmp2 = (OR) tmp1 (((ucast et_val)::word32) << 5); 
      tmp3 = (OR) tmp2 (((ucast s_val)::word32) << 7)
  in  
  tmp3
"

definition update_PSR_exe_trap :: "word5 ⇒ word1 ⇒ word1 ⇒ word32 ⇒ word32"
where
"update_PSR_exe_trap cwp_val et_val ps_val psr_val ≡
  let tmp0 = (AND) psr_val 0b11111111111111111111111110000000;
      tmp1 = (OR) tmp0 ((ucast cwp_val)::word32);
      tmp2 = (OR) tmp1 (((ucast et_val)::word32) << 5); 
      tmp3 = (OR) tmp2 (((ucast ps_val)::word32) << 6)
  in  
  tmp3
"

text ‹Update the N, Z, V, C fields of PSR. 
        Return the new value of PSR.›
definition update_PSR_icc :: "word1 ⇒ word1 ⇒ word1 ⇒ word1 ⇒ word32 ⇒ word32"
where
"update_PSR_icc n_val z_val v_val c_val psr_val ≡
  let
      n_val_32 = if n_val = 0 then 0 
                 else       (0b00000000100000000000000000000000::word32); 
      z_val_32 = if z_val = 0 then 0 
                 else       (0b00000000010000000000000000000000::word32); 
      v_val_32 = if v_val = 0 then 0 
                 else       (0b00000000001000000000000000000000::word32);
      c_val_32 = if c_val = 0 then 0 
                 else       (0b00000000000100000000000000000000::word32);
      tmp0 = (AND) psr_val (0b11111111000011111111111111111111::word32);
      tmp1 = (OR) tmp0 n_val_32;
      tmp2 = (OR) tmp1 z_val_32;
      tmp3 = (OR) tmp2 v_val_32;
      tmp4 = (OR) tmp3 c_val_32
  in
  tmp4
"

text ‹Update the ET, PIL fields of PSR. 
        Return the new value of PSR.›
definition update_PSR_et_pil :: "word1 ⇒ word4 ⇒ word32 ⇒ word32"
where
"update_PSR_et_pil et pil psr_val ≡
  let tmp0 = (AND) psr_val 0b111111111111111111111000011011111;
      tmp1 = (OR) tmp0 (((ucast et)::word32) << 5);
      tmp2 = (OR) tmp1 (((ucast pil)::word32) << 8)
  in
  tmp2
"

text ‹
   SPARC V8 architecture is organized in windows of 32 user registers.
   The data stored in a register is defined as a 32 bits word @{term reg_type}:
›
type_synonym reg_type = "word32"

text ‹
  The access to the value of a CPU register of type @{term CPU_register} is
  defined by a total function @{term cpu_context}
›

type_synonym cpu_context = "CPU_register ⇒ reg_type"

text ‹
  User registers are defined with the type @{term user_reg} represented by a 5 bits word.
›

type_synonym user_reg_type = "word5"

definition PSR_S ::"reg_type"
where "PSR_S ≡ 6"
text ‹
  Each window context is defined by a total function @{term window_context} from @{term user_register} 
  to @{term reg_type} (32 bits word storing the actual value of the register).
›

type_synonym window_context = "user_reg_type ⇒ reg_type"
text ‹
  The number of windows is implementation dependent. 
  The LEON architecture is composed of 16 different windows (a 4 bits word).
›

definition NWINDOWS :: "int"
where "NWINDOWS ≡ 8"

text ‹Maximum number of windows is 32 in SPARCv8.›
type_synonym ('a) window_size = "'a word"

text ‹
Finally the user context is defined by another total function @{term user_context} from 
@{term window_size} to @{term window_context}. That is, the user context is a function taking as
argument a register set window and a register within that window, and it returns the value stored
in that user register.
›
type_synonym ('a) user_context = "('a) window_size ⇒ window_context"

datatype sys_reg = 
         CCR    ― ‹Cache control register›
        |ICCR   ― ‹Instruction cache configuration register›
        |DCCR   ― ‹Data cache configuration register›

type_synonym sys_context = "sys_reg ⇒ reg_type"

text‹
The memory model is defined by a total function from 32 bits words to 8 bits words
›
type_synonym asi_type = "word8"

text ‹
 The memory is defined as a function from page address to page, which is also defined
  as a function from physical address to @{term "machine_word"}
›

type_synonym mem_val_type = "word8"
type_synonym mem_context = "asi_type ⇒ phys_address ⇒ mem_val_type option"

type_synonym cache_tag = "word20"
type_synonym cache_line_size = "word12"
type_synonym cache_type = "(cache_tag × cache_line_size)"
type_synonym cache_context = "cache_type ⇒ mem_val_type option"

text ‹The delayed-write pool generated from write state register instructions.›
type_synonym delayed_write_pool = "(int × reg_type × CPU_register) list"

definition DELAYNUM :: "int"
where "DELAYNUM ≡ 0"

text ‹Convert a set to a list.›
definition list_of_set :: "'a set ⇒ 'a list"
  where "list_of_set s = (SOME l. set l = s)"

lemma set_list_of_set: "finite s ⟹ set (list_of_set s) = s"
unfolding list_of_set_def 
by (metis (mono_tags) finite_list some_eq_ex)

type_synonym ANNUL = "bool"
type_synonym RESET_TRAP = "bool"
type_synonym EXECUTE_MODE = "bool"
type_synonym RESET_MODE = "bool"
type_synonym ERROR_MODE = "bool"
type_synonym TICC_TRAP_TYPE = "word7"
type_synonym INTERRUPT_LEVEL = "word3"
type_synonym STORE_BARRIER_PENDING = "bool"

text ‹The processor asserts this signal to ensure that the
memory system will not process another SWAP or
LDSTUB operation to the same memory byte.›
type_synonym pb_block_ldst_byte = "virtua_address ⇒ bool"

text‹The processor asserts this signal to ensure that the
memory system will not process another SWAP or
LDSTUB operation to the same memory word.›
type_synonym pb_block_ldst_word = "virtua_address ⇒ bool"

record sparc_state_var =
annul:: ANNUL
resett:: RESET_TRAP
exe:: EXECUTE_MODE
reset:: RESET_MODE
err:: ERROR_MODE
ticc:: TICC_TRAP_TYPE
itrpt_lvl:: INTERRUPT_LEVEL
st_bar:: STORE_BARRIER_PENDING
atm_ldst_byte:: pb_block_ldst_byte
atm_ldst_word:: pb_block_ldst_word

definition get_annul :: "sparc_state_var ⇒ bool"
where "get_annul v ≡ annul v"

definition get_reset_trap :: "sparc_state_var ⇒ bool"
where "get_reset_trap v ≡ resett v"

definition get_exe_mode :: "sparc_state_var ⇒ bool"
where "get_exe_mode v ≡ exe v"

definition get_reset_mode :: "sparc_state_var ⇒ bool"
where "get_reset_mode v ≡ reset v"

definition get_err_mode :: "sparc_state_var ⇒ bool"
where "get_err_mode v ≡ err v"

definition get_ticc_trap_type :: "sparc_state_var ⇒ word7"
where "get_ticc_trap_type v ≡ ticc v"

definition get_interrupt_level :: "sparc_state_var ⇒ word3"
where "get_interrupt_level v ≡ itrpt_lvl v"

definition get_store_barrier_pending :: "sparc_state_var ⇒ bool"
where "get_store_barrier_pending v ≡ st_bar v"

definition write_annul :: "bool ⇒ sparc_state_var ⇒ sparc_state_var"
where "write_annul b v ≡ v⦇annul := b⦈"

definition write_reset_trap :: "bool ⇒ sparc_state_var ⇒ sparc_state_var"
where "write_reset_trap b v ≡ v⦇resett := b⦈"

definition write_exe_mode :: "bool ⇒ sparc_state_var ⇒ sparc_state_var"
where "write_exe_mode b v ≡ v⦇exe := b⦈"

definition write_reset_mode :: "bool ⇒ sparc_state_var ⇒ sparc_state_var"
where "write_reset_mode b v ≡ v⦇reset := b⦈"

definition write_err_mode :: "bool ⇒ sparc_state_var ⇒ sparc_state_var"
where "write_err_mode b v ≡ v⦇err := b⦈"

definition write_ticc_trap_type :: "word7 ⇒ sparc_state_var ⇒ sparc_state_var"
where "write_ticc_trap_type w v ≡ v⦇ticc := w⦈"

definition write_interrupt_level :: "word3 ⇒ sparc_state_var ⇒ sparc_state_var"
where "write_interrupt_level w v ≡ v⦇itrpt_lvl := w⦈"

definition write_store_barrier_pending :: "bool ⇒ sparc_state_var ⇒ sparc_state_var"
where "write_store_barrier_pending b v ≡ v⦇st_bar := b⦈"

text ‹Given a word7 value, find the highest bit,
        and fill the left bits to be the highest bit.›
definition sign_ext7::"word7 ⇒ word32"
where
"sign_ext7 w ≡ 
  let highest_bit = ((AND) w 0b1000000) >> 6 in
  if highest_bit = 0 then
    (ucast w)::word32
  else (OR) ((ucast w)::word32) 0b11111111111111111111111110000000
"

definition zero_ext8 :: "word8 ⇒ word32"
where
"zero_ext8 w ≡ (ucast w)::word32
"

text ‹Given a word8 value, find the highest bit,
        and fill the left bits to be the highest bit.›
definition sign_ext8::"word8 ⇒ word32"
where
"sign_ext8 w ≡ 
  let highest_bit = ((AND) w 0b10000000) >> 7 in
  if highest_bit = 0 then
    (ucast w)::word32
  else (OR) ((ucast w)::word32) 0b11111111111111111111111100000000
"

text ‹Given a word13 value, find the highest bit,
        and fill the left bits to be the highest bit.›
definition sign_ext13::"word13 ⇒ word32"
where
"sign_ext13 w ≡ 
  let highest_bit = ((AND) w 0b1000000000000) >> 12 in
  if highest_bit = 0 then
    (ucast w)::word32
  else (OR) ((ucast w)::word32) 0b11111111111111111110000000000000
"

definition zero_ext16 :: "word16 ⇒ word32"
where
"zero_ext16 w ≡ (ucast w)::word32
"

text ‹Given a word16 value, find the highest bit,
        and fill the left bits to be the highest bit.›
definition sign_ext16::"word16 ⇒ word32"
where
"sign_ext16 w ≡ 
  let highest_bit = ((AND) w 0b1000000000000000) >> 15 in
  if highest_bit = 0 then
    (ucast w)::word32
  else (OR) ((ucast w)::word32) 0b11111111111111110000000000000000
"

text ‹Given a word22 value, find the highest bit,
        and fill the left bits to tbe the highest bit.›
definition sign_ext22::"word22 ⇒ word32"
where
"sign_ext22 w ≡
  let highest_bit = ((AND) w 0b1000000000000000000000) >> 21 in
  if highest_bit = 0 then
    (ucast w)::word32
  else (OR) ((ucast w)::word32) 0b11111111110000000000000000000000
"

text ‹Given a word24 value, find the highest bit,
        and fill the left bits to tbe the highest bit.›
definition sign_ext24::"word24 ⇒ word32"
where
"sign_ext24 w ≡
  let highest_bit = ((AND) w 0b100000000000000000000000) >> 23 in
  if highest_bit = 0 then
    (ucast w)::word32
  else (OR) ((ucast w)::word32) 0b11111111000000000000000000000000
"

text‹
Operations to be defined.
The SPARC V8 architecture is composed of the following set of instructions:
  ▪ Load Integer Instructions
  ▪ Load Floating-point Instructions
  ▪ Load Coprocessor Instructions
  ▪ Store Integer Instructions
  ▪ Store Floating-point Instructions
  ▪ Store Coprocessor Instructions
  ▪ Atomic Load-Store Unsigned Byte Instructions
  ▪ SWAP Register With Memory Instruction
  ▪ SETHI Instructions
  ▪ NOP Instruction
  ▪ Logical Instructions
  ▪ Shift Instructions
  ▪ Add Instructions
  ▪ Tagged Add Instructions
  ▪ Subtract Instructions
  ▪ Tagged Subtract Instructions
  ▪ Multiply Step Instruction
  ▪ Multiply Instructions
  ▪ Divide Instructions
  ▪ SAVE and RESTORE Instructions
  ▪ Branch on Integer Condition Codes Instructions
  ▪ Branch on Floating-point Condition Codes Instructions
  ▪ Branch on Coprocessor Condition Codes Instructions
  ▪ Call and Link Instruction
  ▪ Jump and Link Instruction
  ▪ Return from Trap Instruction
  ▪ Trap on Integer Condition Codes Instructions
  ▪ Read State Register Instructions
  ▪ Write State Register Instructions
  ▪ STBAR Instruction
  ▪ Unimplemented Instruction
  ▪ Flush Instruction Memory
  ▪ Floating-point Operate (FPop) Instructions
  ▪ Convert Integer to Floating point Instructions
  ▪ Convert Floating point to Integer Instructions
  ▪ Convert Between Floating-point Formats Instructions
  ▪ Floating-point Move Instructions
  ▪ Floating-point Square Root Instructions
  ▪ Floating-point Add and Subtract Instructions
  ▪ Floating-point Multiply and Divide Instructions
  ▪ Floating-point Compare Instructions
  ▪ Coprocessor Operate Instructions
›

text ‹The CALL instruction.›
datatype call_type = CALL ― ‹Call and Link›

text ‹The SETHI instruction.›
datatype sethi_type = SETHI    ― ‹Set High 22 bits of r Register›

text ‹The NOP instruction.›
datatype nop_type = NOP      ― ‹No Operation›

text ‹The Branch on integer condition codes instructions.› 
datatype bicc_type = 
  BE       ― ‹Branch on Equal›
 | BNE      ― ‹Branch on Not Equal›
 | BGU      ― ‹Branch on Greater Unsigned›
 | BLE      ― ‹Branch on Less or Equal›
 | BL       ― ‹Branch on Less›
 | BGE      ― ‹Branch on Greater or Equal›
 | BNEG     ― ‹Branch on Negative›
 | BG       ― ‹Branch on Greater›
 | BCS      ― ‹Branch on Carry Set (Less than, Unsigned)›
 | BLEU     ― ‹Branch on Less or Equal Unsigned›
 | BCC      ― ‹Branch on Carry Clear (Greater than or Equal, Unsigned)›
 | BA       ― ‹Branch Always›
 | BN       ― ‹Branch Never› ― ‹Added for unconditional branches›
 | BPOS     ― ‹Branch on Positive›
 | BVC      ― ‹Branch on Overflow Clear›
 | BVS      ― ‹Branch on Overflow Set›

text ‹Memory instructions. That is, load and store.›
datatype load_store_type =
  LDSB     ― ‹Load Signed Byte›
 | LDUB     ― ‹Load Unsigned Byte›
 | LDUBA    ― ‹Load Unsigned Byte from Alternate space›
 | LDUH     ― ‹Load Unsigned Halfword›
 | LD       ― ‹Load Word›
 | LDA      ― ‹Load Word from Alternate space›
 | LDD      ― ‹Load Doubleword›
 | STB      ― ‹Store Byte›
 | STH      ― ‹Store Halfword›
 | ST       ― ‹Store Word›
 | STA      ― ‹Store Word into Alternate space›
 | STD      ― ‹Store Doubleword›
 | LDSBA    ― ‹Load Signed Byte from Alternate space›
 | LDSH     ― ‹Load Signed Halfword›
 | LDSHA    ― ‹Load Signed Halfword from Alternate space›
 | LDUHA    ― ‹Load Unsigned Halfword from Alternate space›
 | LDDA     ― ‹Load Doubleword from Alternate space›
 | STBA     ― ‹Store Byte into Alternate space›
 | STHA     ― ‹Store Halfword into Alternate space›
 | STDA     ― ‹Store Doubleword into Alternate space›
 | LDSTUB   ― ‹Atomic Load Store Unsigned Byte›
 | LDSTUBA  ― ‹Atomic Load Store Unsinged Byte in Alternate space›
 | SWAP     ― ‹Swap r Register with Mmemory›
 | SWAPA    ― ‹Swap r Register with Mmemory in Alternate space›
 | FLUSH    ― ‹Flush Instruction Memory›
 | STBAR    ― ‹Store Barrier›

text ‹Arithmetic instructions.›
datatype arith_type =
  ADD      ― ‹Add›
 | ADDcc    ― ‹Add and modify icc›
 | ADDX     ― ‹Add with Carry›
 | SUB      ― ‹Subtract›
 | SUBcc    ― ‹Subtract and modify icc›
 | SUBX     ― ‹Subtract with Carry›
 | UMUL     ― ‹Unsigned Integer Multiply›
 | SMUL     ― ‹Signed Integer Multiply›
 | SMULcc   ― ‹Signed Integer Multiply and modify icc›
 | UDIV     ― ‹Unsigned Integer Divide›
 | UDIVcc   ― ‹Unsigned Integer Divide and modify icc›
 | SDIV     ― ‹Signed Integer Divide› 
 | ADDXcc   ― ‹Add with Carry and modify icc›
 | TADDcc   ― ‹Tagged Add and modify icc›
 | TADDccTV ― ‹Tagged Add and modify icc and Trap on overflow›
 | SUBXcc   ― ‹Subtract with Carry and modify icc›
 | TSUBcc   ― ‹Tagged Subtract and modify icc›
 | TSUBccTV ― ‹Tagged Subtract and modify icc and Trap on overflow›
 | MULScc   ― ‹Multiply Step and modify icc›
 | UMULcc   ― ‹Unsigned Integer Multiply and modify icc›
 | SDIVcc   ― ‹Signed Integer Divide and modify icc›

text ‹Logical instructions.›
datatype logic_type =
  ANDs      ― ‹And›
 | ANDcc    ― ‹And and modify icc›
 | ANDN     ― ‹And Not›
 | ANDNcc   ― ‹And Not and modify icc›
 | ORs       ― ‹Inclusive-Or›
 | ORcc     ― ‹Inclusive-Or and modify icc›
 | ORN      ― ‹Inclusive Or Not›
 | XORs      ― ‹Exclusive-Or›
 | XNOR     ― ‹Exclusive-Nor›
 | ORNcc    ― ‹Inclusive-Or Not and modify icc›
 | XORcc    ― ‹Exclusive-Or and modify icc›
 | XNORcc   ― ‹Exclusive-Nor and modify icc›
 
text ‹Shift instructions.›
datatype shift_type =
  SLL      ― ‹Shift Left Logical›
 | SRL      ― ‹Shift Right Logical›
 | SRA      ― ‹Shift Right Arithmetic› 

text ‹Other Control-transfer instructions.›
datatype ctrl_type = 
  JMPL     ― ‹Jump and Link›
 | RETT     ― ‹Return from Trap›
 | SAVE     ― ‹Save caller's window›
 | RESTORE  ― ‹Restore caller's window› 

text ‹Access state registers instructions.›
datatype sreg_type =
  RDASR    ― ‹Read Ancillary State Register›
 | RDY      ― ‹Read Y Register›
 | RDPSR    ― ‹Read Processor State Register›
 | RDWIM    ― ‹Read Window Invalid Mask Register›
 | RDTBR    ― ‹Read Trap Base Regiser›
 | WRASR    ― ‹Write Ancillary State Register›
 | WRY      ― ‹Write Y Register›
 | WRPSR    ― ‹Write Processor State Register›
 | WRWIM    ― ‹Write Window Invalid Mask Register›
 | WRTBR    ― ‹Write Trap Base Register› 

text ‹Unimplemented instruction.›
datatype uimp_type = UNIMP    ― ‹Unimplemented› 

text ‹Trap on integer condition code instructions.›
datatype ticc_type =
 TA       ― ‹Trap Always›
 | TN       ― ‹Trap Never›
 | TNE      ― ‹Trap on Not Equal›
 | TE       ― ‹Trap on Equal›
 | TG       ― ‹Trap on Greater›
 | TLE      ― ‹Trap on Less or Equal›
 | TGE      ― ‹Trap on Greater or Equal›
 | TL       ― ‹Trap on Less›
 | TGU      ― ‹Trap on Greater Unsigned›
 | TLEU     ― ‹Trap on Less or Equal Unsigned›
 | TCC      ― ‹Trap on Carry Clear (Greater than or Equal, Unsigned)›
 | TCS      ― ‹Trap on Carry Set (Less Than, Unsigned)›
 | TPOS     ― ‹Trap on Postive›
 | TNEG     ― ‹Trap on Negative›
 | TVC      ― ‹Trap on Overflow Clear›
 | TVS      ― ‹Trap on Overflow Set›

datatype sparc_operation =
  call_type call_type
 | sethi_type sethi_type
 | nop_type nop_type
 | bicc_type bicc_type
 | load_store_type load_store_type
 | arith_type arith_type
 | logic_type logic_type
 | shift_type shift_type
 | ctrl_type ctrl_type
 | sreg_type sreg_type
 | uimp_type uimp_type
 | ticc_type ticc_type

datatype Trap = 
reset 
|data_store_error
|instruction_access_MMU_miss
|instruction_access_error
|r_register_access_error
|instruction_access_exception
|privileged_instruction
|illegal_instruction
|unimplemented_FLUSH
|watchpoint_detected
|fp_disabled
|cp_disabled
|window_overflow
|window_underflow
|mem_address_not_aligned
|fp_exception
|cp_exception
|data_access_error
|data_access_MMU_miss
|data_access_exception
|tag_overflow
|division_by_zero
|trap_instruction
|interrupt_level_n

datatype Exception =
― ‹The following are processor states that are not in the instruction model,›
― ‹but we MAY want to deal with these from hardware perspective.›
⌦‹|execute_mode›
⌦‹|reset_mode›
⌦‹|error_mode›
― ‹The following are self-defined exceptions.›
invalid_cond_f2
|invalid_op2_f2
|illegal_instruction2 ― ‹when ‹i = 0› for load/store not from alternate space›
|invalid_op3_f3_op11
|case_impossible
|invalid_op3_f3_op10
|invalid_op_f3
|unsupported_instruction
|fetch_instruction_error
|invalid_trap_cond

end

(*
 * Copyright 2014, NICTA
 *
 * This software may be distributed and modified according to the terms of
 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
 * See "LICENSE_BSD2.txt" for details.
 *
 * @TAG(NICTA_BSD)
 *)

(*
   Miscellaneous library definitions and lemmas.
*)

(*chapter "Library"*)

theory Lib
imports Main
begin

lemma hd_map_simp:
  "b ≠ [] ⟹ hd (map a b) = a (hd b)"
  by (rule hd_map)

lemma tl_map_simp:
  "tl (map a b) = map a (tl b)"
  by (induct b,auto)

lemma Collect_eq:
  "{x. P x} = {x. Q x} ⟷ (∀x. P x = Q x)"
  by (rule iffI) auto

lemma iff_impI: "⟦P ⟹ Q = R⟧ ⟹ (P ⟶ Q) = (P ⟶ R)" by blast

definition
  fun_app :: "('a ⇒ 'b) ⇒ 'a ⇒ 'b" (infixr "$" 10) where
  "f $ x ≡ f x"

declare fun_app_def [iff]

lemma fun_app_cong[fundef_cong]:
  "⟦ f x = f' x' ⟧ ⟹ (f $ x) = (f' $ x')"
  by simp

lemma fun_app_apply_cong[fundef_cong]:
  "f x y = f' x' y' ⟹ (f $ x) y = (f' $ x') y'"
  by simp

lemma if_apply_cong[fundef_cong]:
  "⟦ P = P'; x = x'; P' ⟹ f x' = f' x'; ¬ P' ⟹ g x' = g' x' ⟧
     ⟹ (if P then f else g) x = (if P' then f' else g') x'"
  by simp

abbreviation (input) split :: "('a ⇒ 'b ⇒ 'c) ⇒ 'a × 'b ⇒ 'c" where
  "split ≡ case_prod"

lemma split_apply_cong[fundef_cong]:
  "⟦ f (fst p) (snd p) s = f' (fst p') (snd p') s' ⟧ ⟹ split f p s = split f' p' s'"
  by (simp add: split_def)

definition
  pred_conj :: "('a ⇒ bool) ⇒ ('a ⇒ bool) ⇒ ('a ⇒ bool)" (infixl "and" 35)
where
  "pred_conj P Q ≡ λx. P x ∧ Q x"

definition
  pred_disj :: "('a ⇒ bool) ⇒ ('a ⇒ bool) ⇒ ('a ⇒ bool)" (infixl "or" 30)
where
  "pred_disj P Q ≡ λx. P x ∨ Q x"

definition
  pred_neg :: "('a ⇒ bool) ⇒ ('a ⇒ bool)" ("not _" [40] 40)
where
  "pred_neg P ≡ λx. ¬ P x"

definition "K ≡ λx y. x"

definition
  zipWith :: "('a ⇒ 'b ⇒ 'c) ⇒ 'a list ⇒ 'b list ⇒ 'c list" where
  "zipWith f xs ys ≡ map (split f) (zip xs ys)"

primrec
  delete :: "'a ⇒ 'a list ⇒ 'a list"
where
  "delete y [] = []"
| "delete y (x#xs) = (if y=x then xs else x # delete y xs)"

primrec
  find :: "('a ⇒ bool) ⇒ 'a list ⇒ 'a option"
where
  "find f [] = None"
| "find f (x # xs) = (if f x then Some x else find f xs)"

definition
 "swp f ≡ λx y. f y x"

primrec (nonexhaustive)
  theRight :: "'a + 'b ⇒ 'b" where
  "theRight (Inr x) = x"

primrec (nonexhaustive)
  theLeft :: "'a + 'b ⇒ 'a" where
  "theLeft (Inl x) = x"

definition
 "isLeft x ≡ (∃y. x = Inl y)"

definition
 "isRight x ≡ (∃y. x = Inr y)"

definition
 "const x ≡ λy. x"

lemma tranclD2:
  "(x, y) ∈ R⇧+ ⟹ ∃z. (x, z) ∈ R⇧* ∧ (z, y) ∈ R"
  by (erule tranclE) auto

lemma linorder_min_same1 [simp]:
  "(min y x = y) = (y ≤ (x::'a::linorder))"
  by (auto simp: min_def linorder_not_less)

lemma linorder_min_same2 [simp]:
  "(min x y = y) = (y ≤ (x::'a::linorder))"
  by (auto simp: min_def linorder_not_le)

text ‹A combinator for pairing up well-formed relations.
        The divisor function splits the population in halves,
        with the True half greater than the False half, and
        the supplied relations control the order within the halves.›

definition
  wf_sum :: "('a ⇒ bool) ⇒ ('a × 'a) set ⇒ ('a × 'a) set ⇒ ('a × 'a) set"
where
  "wf_sum divisor r r' ≡
     ({(x, y). ¬ divisor x ∧ ¬ divisor y} ∩ r')
   ∪  {(x, y). ¬ divisor x ∧ divisor y}
   ∪ ({(x, y). divisor x ∧ divisor y} ∩ r)"

lemma wf_sum_wf:
  "⟦ wf r; wf r' ⟧ ⟹ wf (wf_sum divisor r r')"
  apply (simp add: wf_sum_def)
  apply (rule wf_Un)+
      apply (erule wf_Int2)
     apply (rule wf_subset
             [where r="measure (λx. If (divisor x) 1 0)"])
      apply simp
     apply clarsimp
    apply blast
   apply (erule wf_Int2)
  apply blast
  done

abbreviation(input)
 "option_map == map_option"

lemmas option_map_def = map_option_case

lemma False_implies_equals [simp]:
  "((False ⟹ P) ⟹ PROP Q) ≡ PROP Q"
  apply (rule equal_intr_rule)
   apply (erule meta_mp)
   apply simp
  apply simp
  done

lemma split_paired_Ball:
  "(∀x ∈ A. P x) = (∀x y. (x,y) ∈ A ⟶ P (x,y))"
  by auto

lemma split_paired_Bex:
  "(∃x ∈ A. P x) = (∃x y. (x,y) ∈ A ∧ P (x,y))"
  by auto

end

(*
 * Copyright 2014, NICTA
 *
 * This software may be distributed and modified according to the terms of
 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
 * See "LICENSE_BSD2.txt" for details.
 *
 * @TAG(NICTA_BSD)
 *)

(*
* Zhe Hou: I modified this file to model a deterministic monad instead of
* a non-deterministic monad. Features that are irrelevant to deterministic 
* moands are removed. I also removed the section for loops, which are not
* used in the modelling of the SPARC architecture.
*)

(* 
   Deterministic state and error monads with failure in Isabelle.
*)

(*chapter "Deterministic State Monad with Failure"*)

theory DetMonad
imports "../Lib"
begin

text ‹
  \label{c:monads}

  State monads are used extensively in the seL4 specification. They are
  defined below.
›

section "The Monad"

text ‹
  The basic type of the deterministic state monad with failure is
  very similar to the normal state monad. Instead of a pair consisting
  of result and new state, we return a pair coupled with
  a failure flag. The flag is @{const True} if the computation have failed. 
  Conversely, if the flag is @{const False}, the computation resulting in 
  the returned result have succeeded.› 
type_synonym ('s,'a) det_monad = "'s ⇒ ('a × 's) × bool"


text ‹
  The definition of fundamental monad functions ‹return› and
  ‹bind›. The monad function ‹return x› does not change 
  the  state, does not fail, and returns ‹x›.
› 
definition
  return :: "'a ⇒ ('s,'a) det_monad" where
  "return a ≡ λs. ((a,s),False)"

text ‹
  The monad function ‹bind f g›, also written ‹f >>= g›,
  is the execution of @{term f} followed by the execution of ‹g›.
  The function ‹g› takes the result value \emph{and} the result
  state of ‹f› as parameter. The definition says that the result of
  the combined operation is the result which is created
  by ‹g› applied to the result of ‹f›. The combined
  operation may have failed, if ‹f› may have failed or ‹g› may
  have failed on the result of ‹f›.
›

text ‹
 David Sanan and Zhe Hou: The original definition of bind is very inefficient 
 when converted to executable code. Here we change it to a more efficient
 version for execution. The idea remains the same.
›

definition "h1 f s = f s"
definition "h2 g fs = (let (a,b) = fst (fs) in g a b)"
definition bind:: "('s, 'a) det_monad ⇒ ('a ⇒ ('s, 'b) det_monad) ⇒ 
           ('s, 'b) det_monad" (infixl ">>=" 60)
where
"bind f g ≡ λs. (
  let fs = h1 f s;
      v = h2 g fs
  in
  (fst v, (snd v ∨ snd fs)))"

text ‹
  Sometimes it is convenient to write ‹bind› in reverse order.
›
abbreviation(input)
  bind_rev :: "('c ⇒ ('a, 'b) det_monad) ⇒ ('a, 'c) det_monad ⇒ 
               ('a, 'b) det_monad" (infixl "=<<" 60) where 
  "g =<< f ≡ f >>= g"

text ‹
  The basic accessor functions of the state monad. ‹get› returns
  the current state as result, does not fail, and does not change the state.
  ‹put s› returns nothing (@{typ unit}), changes the current state
  to ‹s› and does not fail.
›
definition
  get :: "('s,'s) det_monad" where
  "get ≡ λs. ((s,s), False)"

definition
  put :: "'s ⇒ ('s, unit) det_monad" where
  "put s ≡ λ_. (((),s), False)"

subsection "Failure"

text ‹The monad function that always fails. Returns the current 
  state and sets the failure flag.›
definition
  fail :: "'a ⇒ ('s, 'a) det_monad" where
 "fail a ≡ λs. ((a,s), True)"

text ‹Assertions: fail if the property ‹P› is not true›
definition
  assert :: "bool ⇒ ('a, unit) det_monad" where
 "assert P ≡ if P then return () else fail ()"

text ‹An assertion that also can introspect the current state.›

definition
  state_assert :: "('s ⇒ bool) ⇒ ('s, unit) det_monad"
where
  "state_assert P ≡ get >>= (λs. assert (P s))"

subsection "Generic functions on top of the state monad"

text ‹Apply a function to the current state and return the result
without changing the state.›
definition
  gets :: "('s ⇒ 'a) ⇒ ('s, 'a) det_monad" where
 "gets f ≡ get >>= (λs. return (f s))"

text ‹Modify the current state using the function passed in.›
definition
  modify :: "('s ⇒ 's) ⇒ ('s, unit) det_monad" where
 "modify f ≡ get >>= (λs. put (f s))"

lemma simpler_gets_def: "gets f = (λs. ((f s, s), False))"
  apply (simp add: gets_def return_def bind_def h1_def h2_def get_def)
  done

lemma simpler_modify_def:
  "modify f = (λs. (((), f s), False))"
  by (simp add: modify_def bind_def h1_def h2_def get_def put_def)

text ‹Execute the given monad when the condition is true, 
  return ‹()› otherwise.›
definition
  when1 :: "bool ⇒ ('s, unit) det_monad ⇒ 
           ('s, unit) det_monad" where 
  "when1 P m ≡ if P then m else return ()"

text ‹Execute the given monad unless the condition is true, 
  return ‹()› otherwise.›
definition 
  unless :: "bool ⇒ ('s, unit) det_monad ⇒ 
            ('s, unit) det_monad" where
  "unless P m ≡ when1 (¬P) m"

text ‹
  Perform a test on the current state, performing the left monad if
  the result is true or the right monad if the result is false.
›
definition
  condition :: "('s ⇒ bool) ⇒ ('s, 'r) det_monad ⇒ ('s, 'r) det_monad ⇒ ('s, 'r) det_monad"
where
  "condition P L R ≡ λs. if (P s) then (L s) else (R s)"

notation (output)
  condition  ("(condition (_)//  (_)//  (_))" [1000,1000,1000] 1000)

subsection ‹The Monad Laws›

text ‹Each monad satisfies at least the following three laws.›

text ‹@{term return} is absorbed at the left of a @{term bind}, 
  applying the return value directly:› 
lemma return_bind [simp]: "(return x >>= f) = f x"
  by (simp add: return_def bind_def h1_def h2_def)

text ‹@{term return} is absorbed on the right of a @{term bind}› 
lemma bind_return [simp]: "(m >>= return) = m"
  apply (rule ext)
  apply (simp add: bind_def h1_def h2_def return_def split_def)
  done
 
text ‹@{term bind} is associative›
lemma bind_assoc: 
  fixes m :: "('a,'b) det_monad"
  fixes f :: "'b ⇒ ('a,'c) det_monad"
  fixes g :: "'c ⇒ ('a,'d) det_monad"
  shows "(m >>= f) >>= g  =  m >>= (λx. f x >>= g)"
  apply (unfold bind_def h1_def h2_def Let_def split_def)
  apply (rule ext)
  apply clarsimp
  done


section ‹Adding Exceptions›

text ‹
  The type @{typ "('s,'a) det_monad"} gives us determinism and
  failure. We now extend this monad with exceptional return values
  that abort normal execution, but can be handled explicitly.
  We use the sum type to indicate exceptions. 

  In @{typ "('s, 'e + 'a) det_monad"}, @{typ "'s"} is the state,
  @{typ 'e} is an exception, and @{typ 'a} is a normal return value.

  This new type itself forms a monad again. Since type classes in 
  Isabelle are not powerful enough to express the class of monads,
  we provide new names for the @{term return} and @{term bind} functions
  in this monad. We call them ‹returnOk› (for normal return values)
  and ‹bindE› (for composition). We also define ‹throwError›
  to return an exceptional value.
›
definition
  returnOk :: "'a ⇒ ('s, 'e + 'a) det_monad" where
  "returnOk ≡ return o Inr"

definition
  throwError :: "'e ⇒ ('s, 'e + 'a) det_monad" where
  "throwError ≡ return o Inl"

text ‹
  Lifting a function over the exception type: if the input is an
  exception, return that exception; otherwise continue execution.
›
definition
  lift :: "('a ⇒ ('s, 'e + 'b) det_monad) ⇒ 
           'e +'a ⇒ ('s, 'e + 'b) det_monad"
where
  "lift f v ≡ case v of Inl e ⇒ throwError e
                      | Inr v' ⇒ f v'"

text ‹
  The definition of @{term bind} in the exception monad (new
  name ‹bindE›): the same as normal @{term bind}, but 
  the right-hand side is skipped if the left-hand side
  produced an exception.
›
definition
  bindE :: "('s, 'e + 'a) det_monad ⇒ 
            ('a ⇒ ('s, 'e + 'b) det_monad) ⇒ 
            ('s, 'e + 'b) det_monad"  (infixl ">>=E" 60)
where
  "bindE f g ≡ bind f (lift g)"


text ‹
  Lifting a normal deterministic monad into the 
  exception monad is achieved by always returning its
  result as normal result and never throwing an exception.
›
definition
  liftE :: "('s,'a) det_monad ⇒ ('s, 'e+'a) det_monad"
where
  "liftE f ≡ f >>= (λr. return (Inr r))"


text ‹
  Since the underlying type and ‹return› function changed, 
  we need new definitions for when and unless:
›
definition
  whenE :: "bool ⇒ ('s, 'e + unit) det_monad ⇒ 
            ('s, 'e + unit) det_monad" 
  where
  "whenE P f ≡ if P then f else returnOk ()"

definition
  unlessE :: "bool ⇒ ('s, 'e + unit) det_monad ⇒ 
            ('s, 'e + unit) det_monad" 
  where
  "unlessE P f ≡ if P then returnOk () else f"


text ‹
  Throwing an exception when the parameter is @{term None}, otherwise
  returning @{term "v"} for @{term "Some v"}.
›
definition
  throw_opt :: "'e ⇒ 'a option ⇒ ('s, 'e + 'a) det_monad" where
  "throw_opt ex x ≡ 
  case x of None ⇒ throwError ex | Some v ⇒ returnOk v"

subsection "Monad Laws for the Exception Monad"

text ‹More direct definition of @{const liftE}:›
lemma liftE_def2:
  "liftE f = (λs. ((λ(v,s'). (Inr v, s'))  (fst (f s)), snd (f s)))"
  by (auto simp: Let_def liftE_def return_def split_def bind_def h1_def h2_def)
  
text ‹Left @{const returnOk} absorbtion over @{term bindE}:›
lemma returnOk_bindE [simp]: "(returnOk x >>=E f) = f x"
  apply (unfold bindE_def returnOk_def)
  apply (clarsimp simp: lift_def)
  done

lemma lift_return [simp]:
  "lift (return ∘ Inr) = return"
  by (rule ext)
     (simp add: lift_def throwError_def split: sum.splits)

text ‹Right @{const returnOk} absorbtion over @{term bindE}:›
lemma bindE_returnOk [simp]: "(m >>=E returnOk) = m"
  by (simp add: bindE_def returnOk_def)

text ‹Associativity of @{const bindE}:›
lemma bindE_assoc:
  "(m >>=E f) >>=E g = m >>=E (λx. f x >>=E g)"
  apply (simp add: bindE_def bind_assoc)
  apply (rule arg_cong [where f="λx. m >>= x"])
  apply (rule ext)
  apply (case_tac x, simp_all add: lift_def throwError_def)
  done

text ‹@{const returnOk} could also be defined via @{const liftE}:›
lemma returnOk_liftE:
  "returnOk x = liftE (return x)"
  by (simp add: liftE_def returnOk_def)

text ‹Execution after throwing an exception is skipped:›
lemma throwError_bindE [simp]:
  "(throwError E >>=E f) = throwError E"
  by (simp add: bindE_def bind_def h1_def h2_def throwError_def lift_def return_def)


section "Syntax"

text ‹This section defines traditional Haskell-like do-syntax 
  for the state monad in Isabelle.›

subsection "Syntax for the Nondeterministic State Monad"

text ‹We use ‹K_bind› to syntactically indicate the 
  case where the return argument of the left side of a @{term bind}
  is ignored›
definition
  K_bind_def [iff]: "K_bind ≡ λx y. x"

nonterminal
  dobinds and dobind and nobind

syntax
  "_dobind"    :: "[pttrn, 'a] => dobind"             ("(_ ←/ _)" 10)
  ""           :: "dobind => dobinds"                 ("_")
  "_nobind"    :: "'a => dobind"                      ("_")
  "_dobinds"   :: "[dobind, dobinds] => dobinds"      ("(_);//(_)")

  "_do"        :: "[dobinds, 'a] => 'a"               ("(do ((_);//(_))//od)" 100)
translations
  "_do (_dobinds b bs) e"  == "_do b (_do bs e)"
  "_do (_nobind b) e"      == "b >>= (CONST K_bind e)"
  "do x ← a; e od"        == "a >>= (λx. e)"  

text ‹Syntax examples:›
lemma "do x ← return 1; 
          return (2::nat); 
          return x 
       od = 
       return 1 >>= 
       (λx. return (2::nat) >>= 
            K_bind (return x))" 
  by (rule refl)

lemma "do x ← return 1; 
          return 2; 
          return x 
       od = return 1" 
  by simp

subsection "Syntax for the Exception Monad"

text ‹
  Since the exception monad is a different type, we
  need to syntactically distinguish it in the syntax.
  We use ‹doE›/‹odE› for this, but can re-use
  most of the productions from ‹do›/‹od›
  above.
›

syntax
  "_doE" :: "[dobinds, 'a] => 'a"  ("(doE ((_);//(_))//odE)" 100)

translations
  "_doE (_dobinds b bs) e"  == "_doE b (_doE bs e)"
  "_doE (_nobind b) e"      == "b >>=E (CONST K_bind e)"
  "doE x ← a; e odE"       == "a >>=E (λx. e)"

text ‹Syntax examples:›
lemma "doE x ← returnOk 1; 
           returnOk (2::nat); 
           returnOk x 
       odE =
       returnOk 1 >>=E 
       (λx. returnOk (2::nat) >>=E 
            K_bind (returnOk x))"
  by (rule refl)

lemma "doE x ← returnOk 1; 
           returnOk 2; 
           returnOk x 
       odE = returnOk 1" 
  by simp



section "Library of Monadic Functions and Combinators"


text ‹Lifting a normal function into the monad type:›
definition
  liftM :: "('a ⇒ 'b) ⇒ ('s,'a) det_monad ⇒ ('s, 'b) det_monad"
where
  "liftM f m ≡ do x ← m; return (f x) od"

text ‹The same for the exception monad:›
definition
  liftME :: "('a ⇒ 'b) ⇒ ('s,'e+'a) det_monad ⇒ ('s,'e+'b) det_monad"
where
  "liftME f m ≡ doE x ← m; returnOk (f x) odE"

text ‹
  Run a sequence of monads from left to right, ignoring return values.›
definition
  sequence_x :: "('s, 'a) det_monad list ⇒ ('s, unit) det_monad" 
where
  "sequence_x xs ≡ foldr (λx y. x >>= (λ_. y)) xs (return ())"

text ‹
  Map a monadic function over a list by applying it to each element
  of the list from left to right, ignoring return values.
›
definition
  mapM_x :: "('a ⇒ ('s,'b) det_monad) ⇒ 'a list ⇒ ('s, unit) det_monad"
where
  "mapM_x f xs ≡ sequence_x (map f xs)"

text ‹
  Map a monadic function with two parameters over two lists,
  going through both lists simultaneously, left to right, ignoring
  return values.
›
definition
  zipWithM_x :: "('a ⇒ 'b ⇒ ('s,'c) det_monad) ⇒ 
                 'a list ⇒ 'b list ⇒ ('s, unit) det_monad"
where
  "zipWithM_x f xs ys ≡ sequence_x (zipWith f xs ys)"


text ‹The same three functions as above, but returning a list of
return values instead of ‹unit››
definition
  sequence :: "('s, 'a) det_monad list ⇒ ('s, 'a list) det_monad" 
where
  "sequence xs ≡ let mcons = (λp q. p >>= (λx. q >>= (λy. return (x#y))))
                 in foldr mcons xs (return [])"

definition
  mapM :: "('a ⇒ ('s,'b) det_monad) ⇒ 'a list ⇒ ('s, 'b list) det_monad"
where
  "mapM f xs ≡ sequence (map f xs)"

definition
  zipWithM :: "('a ⇒ 'b ⇒ ('s,'c) det_monad) ⇒ 
                 'a list ⇒ 'b list ⇒ ('s, 'c list) det_monad"
where
  "zipWithM f xs ys ≡ sequence (zipWith f xs ys)"

definition
  foldM :: "('b ⇒ 'a ⇒ ('s, 'a) det_monad) ⇒ 'b list ⇒ 'a ⇒ ('s, 'a) det_monad" 
where
  "foldM m xs a ≡ foldr (λp q. q >>= m p) xs (return a) "

text ‹The sequence and map functions above for the exception monad,
with and without lists of return value›
definition
  sequenceE_x :: "('s, 'e+'a) det_monad list ⇒ ('s, 'e+unit) det_monad" 
where
  "sequenceE_x xs ≡ foldr (λx y. doE _ ← x; y odE) xs (returnOk ())"

definition
  mapME_x :: "('a ⇒ ('s,'e+'b) det_monad) ⇒ 'a list ⇒ 
              ('s,'e+unit) det_monad"
where
  "mapME_x f xs ≡ sequenceE_x (map f xs)"

definition
  sequenceE :: "('s, 'e+'a) det_monad list ⇒ ('s, 'e+'a list) det_monad" 
where
  "sequenceE xs ≡ let mcons = (λp q. p >>=E (λx. q >>=E (λy. returnOk (x#y))))
                 in foldr mcons xs (returnOk [])"

definition
  mapME :: "('a ⇒ ('s,'e+'b) det_monad) ⇒ 'a list ⇒ 
              ('s,'e+'b list) det_monad"
where
  "mapME f xs ≡ sequenceE (map f xs)"


text ‹Filtering a list using a monadic function as predicate:›
primrec
  filterM :: "('a ⇒ ('s, bool) det_monad) ⇒ 'a list ⇒ ('s, 'a list) det_monad"
where
  "filterM P []       = return []"
| "filterM P (x # xs) = do
     b  ← P x;
     ys ← filterM P xs; 
     return (if b then (x # ys) else ys)
   od"


section "Catching and Handling Exceptions"

text ‹
  Turning an exception monad into a normal state monad
  by catching and handling any potential exceptions:
›
definition
  catch :: "('s, 'e + 'a) det_monad ⇒
            ('e ⇒ ('s, 'a) det_monad) ⇒
            ('s, 'a) det_monad" (infix "<catch>" 10)
where
  "f <catch> handler ≡
     do x ← f;
        case x of
          Inr b ⇒ return b
        | Inl e ⇒ handler e
     od"

text ‹
  Handling exceptions, but staying in the exception monad.
  The handler may throw a type of exceptions different from
  the left side.
›
definition
  handleE' :: "('s, 'e1 + 'a) det_monad ⇒
               ('e1 ⇒ ('s, 'e2 + 'a) det_monad) ⇒
               ('s, 'e2 + 'a) det_monad" (infix "<handle2>" 10)
where
  "f <handle2> handler ≡
   do
      v ← f;
      case v of
        Inl e ⇒ handler e
      | Inr v' ⇒ return (Inr v')
   od"

text ‹
  A type restriction of the above that is used more commonly in
  practice: the exception handle (potentially) throws exception
  of the same type as the left-hand side.
›
definition
  handleE :: "('s, 'x + 'a) det_monad ⇒ 
              ('x ⇒ ('s, 'x + 'a) det_monad) ⇒ 
              ('s, 'x + 'a) det_monad" (infix "<handle>" 10)
where
  "handleE ≡ handleE'"


text ‹
  Handling exceptions, and additionally providing a continuation
  if the left-hand side throws no exception:
›
definition
  handle_elseE :: "('s, 'e + 'a) det_monad ⇒
                   ('e ⇒ ('s, 'ee + 'b) det_monad) ⇒
                   ('a ⇒ ('s, 'ee + 'b) det_monad) ⇒
                   ('s, 'ee + 'b) det_monad"
  ("_ <handle> _ <else> _" 10)
where
  "f <handle> handler <else> continue ≡
   do v ← f;
   case v of Inl e  ⇒ handler e
           | Inr v' ⇒ continue v'
   od"

section "Hoare Logic"

subsection "Validity"

text ‹This section defines a Hoare logic for partial correctness for
  the deterministic state monad as well as the exception monad.
  The logic talks only about the behaviour part of the monad and ignores
  the failure flag.

  The logic is defined semantically. Rules work directly on the
  validity predicate.

  In the deterministic state monad, validity is a triple of precondition,
  monad, and postcondition. The precondition is a function from state to 
  bool (a state predicate), the postcondition is a function from return value
  to state to bool. A triple is valid if for all states that satisfy the
  precondition, all result values and result states that are returned by
  the monad satisfy the postcondition. Note that if the computation returns
  the empty set, the triple is trivially valid. This means @{term "assert P"} 
  does not require us to prove that @{term P} holds, but rather allows us
  to assume @{term P}! Proving non-failure is done via separate predicate and
  calculus (see below).
›
definition
  valid :: "('s ⇒ bool) ⇒ ('s,'a) det_monad ⇒ ('a ⇒ 's ⇒ bool) ⇒ bool" 
  ("⦃_⦄/ _ /⦃_⦄")
where
  "⦃P⦄ f ⦃Q⦄ ≡ ∀s. P s ⟶ (∀r s'. ((r,s') = fst (f s) ⟶ Q r s'))"

text ‹
  Validity for the exception monad is similar and build on the standard 
  validity above. Instead of one postcondition, we have two: one for
  normal and one for exceptional results.
›
definition
  validE :: "('s ⇒ bool) ⇒ ('s, 'a + 'b) det_monad ⇒ 
             ('b ⇒ 's ⇒ bool) ⇒ 
             ('a ⇒ 's ⇒ bool) ⇒ bool" 
("⦃_⦄/ _ /(⦃_⦄,/ ⦃_⦄)")
where
  "⦃P⦄ f ⦃Q⦄,⦃E⦄ ≡ ⦃P⦄ f ⦃ λv s. case v of Inr r ⇒ Q r s | Inl e ⇒ E e s ⦄"


text ‹
  The following two instantiations are convenient to separate reasoning
  for exceptional and normal case.
›
definition
  validE_R :: "('s ⇒ bool) ⇒ ('s, 'e + 'a) det_monad ⇒ 
               ('a ⇒ 's ⇒ bool) ⇒ bool"
   ("⦃_⦄/ _ /⦃_⦄, -")
where
 "⦃P⦄ f ⦃Q⦄,- ≡ validE P f Q (λx y. True)"

definition
  validE_E :: "('s ⇒ bool) ⇒  ('s, 'e + 'a) det_monad ⇒ 
               ('e ⇒ 's ⇒ bool) ⇒ bool"
   ("⦃_⦄/ _ /-, ⦃_⦄")
where
 "⦃P⦄ f -,⦃Q⦄ ≡ validE P f (λx y. True) Q"


text ‹Abbreviations for trivial preconditions:›
abbreviation(input)
  top :: "'a ⇒ bool" ("⊤")
where
  "⊤ ≡ λ_. True"

abbreviation(input)
  bottom :: "'a ⇒ bool" ("⊥")
where
  "⊥ ≡ λ_. False"

text ‹Abbreviations for trivial postconditions (taking two arguments):›
abbreviation(input)
  toptop :: "'a ⇒ 'b ⇒ bool" ("⊤⊤")
where
 "⊤⊤ ≡ λ_ _. True"

abbreviation(input)
  botbot :: "'a ⇒ 'b ⇒ bool" ("⊥⊥")
where
 "⊥⊥ ≡ λ_ _. False"

text ‹
  Lifting ‹∧› and ‹∨› over two arguments. 
  Lifting ‹∧› and ‹∨› over one argument is already
  defined (written ‹and› and ‹or›).
›
definition
  bipred_conj :: "('a ⇒ 'b ⇒ bool) ⇒ ('a ⇒ 'b ⇒ bool) ⇒ ('a ⇒ 'b ⇒ bool)" 
  (infixl "And" 96)
where
  "bipred_conj P Q ≡ λx y. P x y ∧ Q x y"

definition
  bipred_disj :: "('a ⇒ 'b ⇒ bool) ⇒ ('a ⇒ 'b ⇒ bool) ⇒ ('a ⇒ 'b ⇒ bool)" 
  (infixl "Or" 91)
where
  "bipred_disj P Q ≡ λx y. P x y ∨ Q x y"


subsection "Determinism"

text ‹A monad of type ‹det_monad› is deterministic iff it
returns exactly one state and result and does not fail› 
definition
  det :: "('a,'s) det_monad ⇒ bool"
where
  "det f ≡ ∀s. ∃r. f s = (r,False)" 

text ‹A deterministic ‹det_monad› can be turned
  into a normal state monad:›
definition
  the_run_state :: "('s,'a) det_monad ⇒ 's ⇒ 'a × 's"
where
  "the_run_state M ≡ λs. THE s'. fst (M s) = s'"


subsection "Non-Failure"

text ‹
  With the failure flag, we can formulate non-failure separately
  from validity. A monad ‹m› does not fail under precondition
  ‹P›, if for no start state in that precondition it sets
  the failure flag.
›
definition
  no_fail :: "('s ⇒ bool) ⇒ ('s,'a) det_monad ⇒ bool"
where
  "no_fail P m ≡ ∀s. P s ⟶ ¬ (snd (m s))"


text ‹
  It is often desired to prove non-failure and a Hoare triple
  simultaneously, as the reasoning is often similar. The following
  definitions allow such reasoning to take place.
›

definition
  validNF ::"('s ⇒ bool) ⇒ ('s,'a) det_monad ⇒ ('a ⇒ 's ⇒ bool) ⇒ bool"
      ("⦃_⦄/ _ /⦃_⦄!")
where
  "validNF P f Q ≡ valid P f Q ∧ no_fail P f"

definition
  validE_NF :: "('s ⇒ bool) ⇒ ('s, 'a + 'b) det_monad ⇒
             ('b ⇒ 's ⇒ bool) ⇒
             ('a ⇒ 's ⇒ bool) ⇒ bool"
  ("⦃_⦄/ _ /(⦃_⦄,/ ⦃_⦄!)")
where
  "validE_NF P f Q E ≡ validE P f Q E ∧ no_fail P f"

lemma validE_NF_alt_def:
  "⦃ P ⦄ B ⦃ Q ⦄,⦃ E ⦄! = ⦃ P ⦄ B ⦃ λv s. case v of Inl e ⇒ E e s | Inr r ⇒ Q r s ⦄!"
  by (clarsimp simp: validE_NF_def validE_def validNF_def)

section "Basic exception reasoning"

text ‹
  The following predicates ‹no_throw› and ‹no_return› allow
  reasoning that functions in the exception monad either do
  no throw an exception or never return normally.
›

definition "no_throw P A ≡ ⦃ P ⦄ A ⦃ λ_ _. True ⦄,⦃ λ_ _. False ⦄"

definition "no_return P A ≡ ⦃ P ⦄ A ⦃λ_ _. False⦄,⦃λ_ _. True ⦄"

end